Inference at * 1 1 
Iof proof for Lemma eq atom eq true elim sqequal:



1. x : Atom
2. y : Atom
3. x =a y ~ tt
  x = y 

latex

 by (\p. let x, y = dest_sqequal (h (-1) p) in 
 by (\p(Assert (mk_equal_term bool_term y y) 

 by (\p(AsTHENL [(Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t
 ) inil_term); SqSubstAtAddr [2] x (-1) 
 ) inil_term); SqSubsTHENL [(Auto_aux (first_nat 1:n
 ) ((first_nat 1:n),(first_nat 4:n)) (first_tok :t) inil_term); Id]]) p) 

latex

 1: 

 1: 4. x =a y = tt
 1:   x = y
 .

Definitions	t  T
Lemmas	btrue wf